a, b:. (a ~ b)  a = b   

latex

Definitions	P  Q, P & Q, P  Q, P  Q, a ~ b, x:A. B(x), P  Q, Prop, t  T, , AB, A, False
Lemmas	nat wf, assoced wf, assoced elim, iff functionality wrt iff